(declare-fun X () (_ FloatingPoint 11 53))
(declare-fun Y () (_ FloatingPoint 9 53))
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
(assert (fp.leq X (fp #b0 #b10011111110 #xFFFFFFFFFFFFF)))
(assert (= Y ((_ to_fp 9 53) RNE X)))
(check-sat)
